Homework (Week 1)

Let \(s\) be a state, and let \(s^\omega\) denote the behaviour \(s s s s s s s s s s s s \dots\) (i.e. infinitely many repetitions of \(s\).)

Give an example of a set \(A\) such that \(s^\omega \in \overline{A}\), but \(s^\omega \notin A\).

1. Let \(\Sigma = \{a,b\}\). That is, we assume there are only two states, \(a\) and \(b\). Consider the property \(P = \{\sigma | \sigma \mbox{ contains exactly one } b\}\). Use Alpern and Schneider's theorem to decompose \(P\) into a safety property \(P_S\) and a liveness property \(P_L\). Simplify them; that is, don't just say \(P_L = \Sigma^\omega \backslash (\overline{P} \backslash P)\) but give something that explains what \(P_L\) is.

2. Assume \(P\) is a safety property. Prove that \(\Sigma^\omega \backslash (\overline{P} \backslash P) = \Sigma^\omega\) using the algebraic laws of set operations.

3. Is the empty property \(\emptyset\) a liveness property? Is it a safety property? Explain.

This question is not for marks, but for a meaningless brownie point

Assuming there are at least two distinct states \(a\) and \(b\), prove that any property \(P\) is the intersection of two liveness properties.

Hint: It is helpful to note that the union of a dense set and any set is itself dense.

Define suitable predicate symbols and give LTL formalisations for the following properties:

1. Once the dragon was slain, the princess lived happily ever after.
2. The dragon was never slain, but the princess lived happily until she didn't.
3. The dragon was slain at least twice.
4. The dragon was slain at most once.
5. Whenever the dragon was slain, the princess did not live happily.

Prove the following logical statements:

\begin{array}{rcl} \Box\Box \varphi & \Leftrightarrow & \Box \varphi \\ \Diamond\bigcirc \varphi & \Leftrightarrow & \bigcirc \Diamond \varphi \\ % \Diamond\Diamond \varphi & \Leftrightarrow & \Diamond \varphi \\ \Box \varphi & \Rightarrow & \Diamond \varphi \\ % \Diamond\Box \varphi & \Rightarrow & \Box\Diamond \varphi \\ % \Diamond\Box\Diamond\varphi & \Leftrightarrow & \Box\Diamond\varphi \\ % \Box\Diamond\Box\varphi & \Leftrightarrow & \Diamond\Box\varphi \\ \end{array}

It may help to use these semantic definitions for \(\Box\) and \(\Diamond\) (derivable from the definition in terms of \(\mathcal{U}\)):

\begin{array}{rcl} \sigma \models \Diamond\varphi & \text{iff} & \exists i \geq 0.\ (\sigma|_i \models \varphi) \\ \sigma \models \Box\varphi & \text{iff} & \forall i \geq 0.\ (\sigma|_i \models \varphi) \end{array}

You may use previously proven identities (both in this question and in lectures) to prove new ones.

Note that two temporal logic formulas \(\phi\) and \(\psi\) are logically equivalent, written \(\varphi \Leftrightarrow \psi\), iff for all behaviours \(\sigma\) it holds that:

\[ \sigma \models \varphi \mbox{ if and only if } \sigma \models \psi \]